module ordreDesPlages

abstract sig PlageHoraire{
	est : set Etat,
	precede : set PlageHoraire 
}
one sig p0,p1,p2,p3,p5,p6,p7 extends PlageHoraire{}

abstract sig Etat {}
one sig prioritaire, nonPrioritaire extends Etat{}

fact toutePlageAUnEtat { 
	all p : PlageHoraire | one e : Etat | p->e in est
}

fact{
	p0.est=prioritaire && 
	p1.est=prioritaire && 
	p2.est=prioritaire && 
	p3.est=prioritaire && 
	p5.est=nonPrioritaire && 
	p6.est=nonPrioritaire && 
	p7.est=nonPrioritaire 
 }
fact preseance{
	all p1,p2 : PlageHoraire | (p1.est in prioritaire && p2.est in nonPrioritaire =>p1->p2 in precede)
}
fact unePlageNeSePrecedePas{
	all p : PlageHoraire | p->p not in precede
}
fact {
	all p1,p2 :PlageHoraire | p1->p2 in precede => p2->p1 not in precede
}
fact {
	all p1,p2,p3 : PlageHoraire | p1->p2 in precede &&p2->p3 in precede => p1->p3 in precede
}
fact {
	all disjoint p1,p2 : PlageHoraire | (p1->p2 in precede|| p2->p1 in precede)
}
run {}

